(set-logic QF_LIA)
(set-info :source |
    Sequential equivalence checking.
    Calypto Design Systems, Inc. <www.calypto.com>
  |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun P_2 () Bool)
(declare-fun P_3 () Int)
(declare-fun P_4 () Bool)
(declare-fun P_5 () Bool)
(declare-fun P_6 () Bool)
(declare-fun P_7 () Bool)
(declare-fun P_8 () Bool)
(declare-fun P_9 () Bool)
(declare-fun P_10 () Bool)
(declare-fun P_11 () Int)
(declare-fun P_12 () Bool)
(declare-fun P_13 () Int)
(declare-fun P_14 () Bool)
(declare-fun P_15 () Int)
(declare-fun P_16 () Int)
(declare-fun P_17 () Int)
(declare-fun P_18 () Bool)
(declare-fun P_19 () Bool)
(declare-fun P_20 () Int)
(declare-fun P_21 () Int)
(declare-fun P_22 () Int)
(declare-fun P_23 () Int)
(declare-fun P_24 () Int)
(declare-fun P_25 () Int)
(declare-fun P_26 () Int)
(declare-fun P_27 () Int)
(declare-fun P_28 () Int)
(declare-fun P_29 () Int)
(assert (<= 0 P_3))
(assert (<= P_3 127))
(assert (<= 0 P_11))
(assert (<= P_11 127))
(assert (<= 0 P_13))
(assert (<= P_13 127))
(assert (<= 0 P_15))
(assert (<= P_15 127))
(assert (<= 0 P_16))
(assert (<= P_16 4294967295))
(assert (<= 0 P_17))
(assert (<= P_17 4294967295))
(assert (<= 0 P_20))
(assert (<= P_20 4294967295))
(assert (<= 0 P_21))
(assert (<= P_21 4294967295))
(assert (<= 0 P_22))
(assert (<= P_22 4294967295))
(assert (<= 0 P_23))
(assert (<= P_23 4294967295))
(assert (<= 0 P_24))
(assert (<= P_24 4294967295))
(assert (<= 0 P_25))
(assert (<= P_25 4294967295))
(assert (<= 0 P_26))
(assert (<= P_26 4294967295))
(assert (<= 0 P_27))
(assert (<= P_27 4294967295))
(assert (<= 0 P_28))
(assert (<= P_28 4294967295))
(assert (<= 0 P_29))
(assert (<= P_29 4294967295))
(declare-fun dz () Int)
(declare-fun rz () Int)
(assert (let ((?v_0 (- 64 P_3))) (let ((?v_1 (ite (not (and P_2 (>= (ite (>= ?v_0 0) ?v_0 (+ ?v_0 256)) 32))) P_2 false))) (let ((?v_20 (ite (not ?v_1) P_4 false))) (let ((?v_2 (or ?v_20 ?v_1))) (let ((?v_3 (ite (not (and ?v_2 P_5)) ?v_2 false))) (let ((?v_19 (ite (not ?v_3) P_6 false))) (let ((?v_4 (or ?v_19 ?v_3))) (let ((?v_5 (ite (not (and ?v_4 P_7)) ?v_4 false))) (let ((?v_18 (ite (not ?v_5) P_8 false))) (let ((?v_6 (or ?v_18 ?v_5))) (let ((?v_17 (not (and ?v_6 P_9)))) (let ((?v_7 (ite ?v_17 ?v_6 false))) (let ((?v_28 (ite (not ?v_7) P_10 false))) (let ((?v_9 (or ?v_28 ?v_7)) (?v_8 (- 64 P_11))) (let ((?v_16 (not (and ?v_9 (>= (ite (>= ?v_8 0) ?v_8 (+ ?v_8 256)) 32))))) (let ((?v_10 (ite ?v_16 ?v_9 false))) (let ((?v_34 (ite (not ?v_10) P_12 false))) (let ((?v_12 (or ?v_34 ?v_10)) (?v_11 (- 64 P_13))) (let ((?v_15 (not (and ?v_12 (>= (ite (>= ?v_11 0) ?v_11 (+ ?v_11 256)) 32))))) (let ((?v_13 (ite ?v_15 ?v_12 false))) (let ((?v_36 (ite (not ?v_13) P_14 false)) (?v_14 (- 64 P_15))) (let ((?v_42 (not (and (or ?v_36 ?v_13) (>= (ite (>= ?v_14 0) ?v_14 (+ ?v_14 256)) 32)))) (?v_27 (not P_19)) (?v_26 (not P_18)) (?v_25 (not P_2)) (?v_24 (not ?v_20)) (?v_23 (not ?v_19)) (?v_22 (not ?v_18))) (let ((?v_39 (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 (ite ?v_26 (ite ?v_27 0 P_20) P_21) P_22) P_23) P_24) P_25)) (?v_32 (not ?v_28))) (let ((?v_41 (ite ?v_32 ?v_39 P_26)) (?v_37 (not ?v_34))) (let ((?v_46 (ite ?v_37 ?v_41 P_27)) (?v_45 (not ?v_36)) (?v_21 (* 18446744073709551616 P_17)) (?v_29 (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 (ite ?v_26 (ite ?v_27 0 (* 4294967296 P_20)) (* 4294967296 P_21)) (* 4294967296 P_22)) (* 4294967296 P_23)) (* 4294967296 P_24)) (* 4294967296 P_25)))) (let ((?v_38 (ite ?v_17 (+ (* 18446744073709551616 P_16) (* 4294967296 P_17)) (+ ?v_21 ?v_29))) (?v_31 (* 79228162514264337593543950336 P_17)) (?v_33 (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 (ite ?v_26 (ite ?v_27 0 (* 18446744073709551616 P_20)) (* 18446744073709551616 P_21)) (* 18446744073709551616 P_22)) (* 18446744073709551616 P_23)) (* 18446744073709551616 P_24)) (* 18446744073709551616 P_25)))) (let ((?v_30 (ite ?v_17 (+ (* 79228162514264337593543950336 P_16) ?v_21) (+ ?v_31 ?v_33))) (?v_35 (ite ?v_32 ?v_29 (* 4294967296 P_26)))) (let ((?v_40 (ite ?v_16 ?v_38 (+ ?v_30 ?v_35)))) (let ((?v_43 (ite ?v_15 (ite ?v_16 (ite ?v_17 (+ (* P_16 4294967296) P_17) (+ (* P_17 4294967296) ?v_39)) (+ ?v_38 ?v_41)) (+ ?v_40 ?v_46))) (?v_44 (ite ?v_15 ?v_40 (+ (ite ?v_16 ?v_30 (+ (ite ?v_17 (+ (* 340282366920938463463374607431768211456 P_16) ?v_31) (+ (* 340282366920938463463374607431768211456 P_17) (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 (ite ?v_26 (ite ?v_27 0 (* 79228162514264337593543950336 P_20)) (* 79228162514264337593543950336 P_21)) (* 79228162514264337593543950336 P_22)) (* 79228162514264337593543950336 P_23)) (* 79228162514264337593543950336 P_24)) (* 79228162514264337593543950336 P_25)))) (ite ?v_32 ?v_33 (* 18446744073709551616 P_26)))) (ite ?v_37 ?v_35 (* 4294967296 P_27)))))) (= (+ (* 18446744073709551616 dz) rz) (- (ite (not ?v_42) (+ ?v_44 (ite (not ?v_45) P_28 (ite (not ?v_37) P_27 (ite (not ?v_32) P_26 (ite (not ?v_22) P_25 (ite (not ?v_23) P_24 (ite (not ?v_24) P_23 (ite (not ?v_25) P_22 (ite (not ?v_26) P_21 (ite ?v_27 P_29 P_20)))))))))) ?v_43) (ite ?v_42 ?v_43 (+ ?v_44 (ite ?v_45 ?v_46 P_28)))))))))))))))))))))))))))))))))))
(assert (> rz 0))
(assert (< rz 18446744073709551616))
(check-sat)
(exit)
